The Boolean satisfiability problem (SAT) is a decision problem whose instance is a Boolean expression written using only AND, OR, NOT, variables, and parentheses. A formula of propositional logic is said to be satisfiable if logical values can be assigned to its variables in a way that makes the formula true.
Hardware assisted SAT solving has attracted much research in recent years. Conventional hardware solvers are slow and capacity limited, rendering them either obsolete and/or severely constrained.